\begin{tabbing}
(\%S\% 
\\[0ex]$\backslash$p. \=let i = var\_of\_hyp (get\_int\_arg `hn` p) p in \+
\\[0ex]
\\[0ex]let z = get\_distinct\_var `zz' p in 
\\[0ex]Assert 
\\[0ex](mk\_\=all\_term z $\mathbb{N}$ \+
\\[0ex](
\-\-\\[0ex]mk\_all\_term\= i $\mathbb{N}$ \+
\\[0ex](mk\=\_implies\_term \+
\\[0ex](mk\_less\_than\_term (mvt i) (
\-\-\\[0ex]mvt \=z)) \=\+\+
\\[0ex](concl p)))) 
\-\\[0ex]p)
\-
\end{tabbing}